COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00003 00003	
C00006 ENDMK
C⊗;

axiom initial:
	want(Joe,Know(Joe,X0))
	k(Joe,Know(Pat,X0))
	k(Joe,Like(Pat,Joe))
;;

axiom simp:
	∀P Q.(want(P,Q) ≡ true(Want(P,Q),W0))
	∀P Q.(k(P,Q) ≡ true(K(P,Q),W0))
	∀Q.(t Q ≡ true(Q,W0))
	∀Q.(f Q ≡ true(F Q,W0))
;;

axiom nec:
	∀Q.(nec Q ≡ ∀W.true(Q,W))
	∀P Q.(nec Q ⊃ nec K(P,Q))
;;

axiom wantdo:
	∀P Q Act.nec(Want(P,Q) And K(P,Occur Do(P,Act) Implies F Q)
Implies Occur Do(P,Act))
;;

axiom likewant:
	∀P1 P2 Q.nec(Like(P1,P2) And K(P1,Want(P2,Q))
Implies Want(P1,Q))
;;

axiom tell:
	∀P1 P2 X.nec(Know(P1,X) Implies Cause(Do(P1,Tell(P2,X)),Know(P2,X)))
	∀P1 P2 Q.nec(K(P1,Q) Implies Cause(Do(P1,Tell(P2,Q)),K(P2,Q)))
;;

axiom future:
	∀Q.nec(Q Implies F Q)
	∀Q.nec(F F Q Implies F Q)
	∀Q1 Q2.nec(F Q1 And Nec Q2 Implies F (Q1 And Q2))
	∀Q.(f Q ≡ true(F Q,W0))
	∀W W1 Q.(true(F Q,W) ≡ ∃W1.(W prec W1 ∧ true(Q,W1)))
;;

axiom prec:
	∀W.(W prec W)
	∀W1 W2 W3.(W1 prec W2 ∧ W2 prec W3 ⊃ W1 prec W3)
;;

axiom cause:
	∀E Q1 Q2.nec(Cause(E,Q1) And Cause(E,Q2) Implies Cause(E,Q1 And Q2))
	∀E Q.nec(Occur E And Cause(E,Q) Implies F Q)
;;

axiom frame:
	∀P1 P2 P P4 X.
nec(Like(P1,P2) Implies Cause(Do(P3,Tell(P4,Z)),Like(P1,P2)))
	∀ P Q E.nec(K(P,Q) Implies Cause(E,K(P,Q)))
	∀ P X E.nec(Know(P,X) Implies Cause(E,Know(P,X)))
;;

axiom know:
	∀P Q W W1.(true(K(P,Q),W) ≡ ∀W1.(a(P,W,W1) ⊃ true(P,W1)))
	∀P W.a(P,W,W)
;;

axiom logic:
	∀Q1 Q2 W.(true(Q1 And Q2,W) ≡ true(Q1,W) ∧ true(Q2,W))
	∀Q1 Q2 W.(true(Q1 Or Q2,W) ≡ true(Q1,W) ∨ true(Q2,W))
	∀Q1 Q2 W.(true(Q1 Implies Q2,W) ≡ true(Q1,W) ⊃ true(Q2,W))
	∀Q1 Q2 W.(true(Q1 Equiv Q2,W) ≡ (true(Q1,W) ≡ true(Q2,W)))
	∀Q W.(true(Not Q,W) ≡ ¬true(Q,W))
;;